Nuprl Lemma : glued-to-self
11,40
postcript
pdf
A
:Type,
es
:ES,
v
:AbsInterface(
A
). glued(
es
;
A
; (
e
.
v
(
e
));
v
;
v
)
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
e
loc
e'
,
E
,
x
.
A
(
x
)
,
let
x
,
y
=
A
in
B
(
x
;
y
)
,
x
:
A
B
(
x
)
,
Type
,
x
:
A
B
(
x
)
,
b
,
ES
,
AbsInterface(
A
)
,
True
,
T
,
P
Q
,
SqStable(
P
)
,
{
x
:
A
|
B
(
x
)}
,
E(
X
)
,
e
X
,
t
.1
,
X
(
e
)
,
Top
,
P
Q
,
P
&
Q
,
P
Q
,
glued(
es
;
B
;
f
;
Ia
;
Ib
)
Lemmas
es-interface
wf
,
event
system
wf
,
glued-Q-R-glued
,
Q-Q-glued-to-self
,
es-E-interface
wf
,
es-interface-val
wf
,
es-E
wf
,
es-is-interface
wf
,
sq
stable
from
decidable
,
decidable
assert
,
assert
wf
,
es-le
wf
origin
A:Type, es:ES, v:AbsInterface(A). glued(es; A; (
e.v(e)); v; v) A:Type, es:ES, v:AbsInterface(A). glued(es; A; (e.v(e)); v; v) 
Tx:A. B(x)
loc e' x.A(x)
B(x)
B(x)
b
T
Q
X
Q Q